\begin{tabbing} sum\_of\_torder($T$;$R$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$a$, $b$, $x$:$T$.\+ \\[0ex](($R$($a$,$x$) \& $R$($b$,$x$)) $\vee$ ($R$($x$,$a$) \& $R$($x$,$b$))) $\Rightarrow$ ((($R$($a$,$b$)) $\vee$ ($a$ = $b$)) $\vee$ ($R$($b$,$a$))) \- \end{tabbing}